The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

if(true, x, y) → x
if(false, x, y) → y
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
app(app(l1, l2), l3) → app(l1, app(l2, l3))
mem(x, nil) → false
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l)
ifmem(true, x, l) → true
ifmem(false, x, l) → mem(x, l)
inter(x, nil) → nil
inter(nil, x) → nil
inter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))
inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Rewrite Strategy: INNERMOST

(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)

The following defined symbols can occur below the 0th argument of ifinter: ifmem, eq, mem
The following defined symbols can occur below the 0th argument of ifmem: eq

Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
app(app(l1, l2), l3) → app(l1, app(l2, l3))
inter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
ifmem(false, x, l) → mem(x, l)
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
mem(x, nil) → false
app(cons(x, l1), l2) → cons(x, app(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)
ifmem(true, x, l) → true
eq(0, 0) → true
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)
app(nil, l) → l
inter(x, nil) → nil
inter(nil, x) → nil
if(true, x, y) → x
if(false, x, y) → y

Rewrite Strategy: INNERMOST

(3) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(4) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2) [1]
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l) [1]
eq(0, s(x)) → false [1]
eq(s(x), 0) → false [1]
eq(s(x), s(y)) → eq(x, y) [1]
ifmem(false, x, l) → mem(x, l) [1]
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2)) [1]
mem(x, nil) → false [1]
app(cons(x, l1), l2) → cons(x, app(l1, l2)) [1]
ifinter(false, x, l1, l2) → inter(l1, l2) [1]
ifmem(true, x, l) → true [1]
eq(0, 0) → true [1]
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1) [1]
app(nil, l) → l [1]
inter(x, nil) → nil [1]
inter(nil, x) → nil [1]
if(true, x, y) → x [1]
if(false, x, y) → y [1]

Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2) [1]
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l) [1]
eq(0, s(x)) → false [1]
eq(s(x), 0) → false [1]
eq(s(x), s(y)) → eq(x, y) [1]
ifmem(false, x, l) → mem(x, l) [1]
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2)) [1]
mem(x, nil) → false [1]
app(cons(x, l1), l2) → cons(x, app(l1, l2)) [1]
ifinter(false, x, l1, l2) → inter(l1, l2) [1]
ifmem(true, x, l) → true [1]
eq(0, 0) → true [1]
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1) [1]
app(nil, l) → l [1]
inter(x, nil) → nil [1]
inter(nil, x) → nil [1]
if(true, x, y) → x [1]
if(false, x, y) → y [1]

The TRS has the following type information:

inter :: cons:nil → cons:nil → cons:nil cons :: 0:s → cons:nil → cons:nil ifinter :: false:true → 0:s → cons:nil → cons:nil → cons:nil mem :: 0:s → cons:nil → false:true ifmem :: false:true → 0:s → cons:nil → false:true eq :: 0:s → 0:s → false:true 0 :: 0:s s :: 0:s → 0:s false :: false:true true :: false:true nil :: cons:nil app :: cons:nil → cons:nil → cons:nil if :: false:true → if → if → if

Rewrite Strategy: INNERMOST

(7) CompletionProof (UPPER BOUND(ID) transformation)

The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:
none

And the following fresh constants:

const

(8) Obligation:

Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2) [1] mem(x, cons(y, l)) → ifmem(eq(x, y), x, l) [1] eq(0, s(x)) → false [1] eq(s(x), 0) → false [1] eq(s(x), s(y)) → eq(x, y) [1] ifmem(false, x, l) → mem(x, l) [1] ifinter(true, x, l1, l2) → cons(x, inter(l1, l2)) [1] mem(x, nil) → false [1] app(cons(x, l1), l2) → cons(x, app(l1, l2)) [1] ifinter(false, x, l1, l2) → inter(l1, l2) [1] ifmem(true, x, l) → true [1] eq(0, 0) → true [1] inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1) [1] app(nil, l) → l [1] inter(x, nil) → nil [1] inter(nil, x) → nil [1] if(true, x, y) → x [1] if(false, x, y) → y [1] The TRS has the following type information: inter :: cons:nil → cons:nil → cons:nil cons :: 0:s → cons:nil → cons:nil ifinter :: false:true → 0:s → cons:nil → cons:nil → cons:nil mem :: 0:s → cons:nil → false:true ifmem :: false:true → 0:s → cons:nil → false:true eq :: 0:s → 0:s → false:true 0 :: 0:s s :: 0:s → 0:s false :: false:true true :: false:true nil :: cons:nil app :: cons:nil → cons:nil → cons:nil if :: false:true → if → if → if const :: if Rewrite Strategy: INNERMOST

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
false => 0
true => 1
nil => 0
const => 0

(10) Obligation:

Complexity RNTS consisting of the following rules:

app(z, z') -{ 1 }→ l :|: z' = l, l >= 0, z = 0
app(z, z') -{ 1 }→ 1 + x + app(l1, l2) :|: x >= 0, z = 1 + x + l1, z' = l2, l1 >= 0, l2 >= 0
eq(z, z') -{ 1 }→ eq(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' = 1 + x, x >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: x >= 0, z = 1 + x, z' = 0
if(z, z', z'') -{ 1 }→ x :|: z' = x, z'' = y, z = 1, x >= 0, y >= 0
if(z, z', z'') -{ 1 }→ y :|: z' = x, z'' = y, x >= 0, y >= 0, z = 0
ifinter(z, z', z'', z1) -{ 1 }→ inter(l1, l2) :|: z' = x, x >= 0, z1 = l2, z'' = l1, l1 >= 0, z = 0, l2 >= 0
ifinter(z, z', z'', z1) -{ 1 }→ 1 + x + inter(l1, l2) :|: z' = x, z = 1, x >= 0, z1 = l2, z'' = l1, l1 >= 0, l2 >= 0
ifmem(z, z', z'') -{ 1 }→ mem(x, l) :|: z' = x, x >= 0, l >= 0, z = 0, z'' = l
ifmem(z, z', z'') -{ 1 }→ 1 :|: z' = x, z = 1, x >= 0, l >= 0, z'' = l
inter(z, z') -{ 1 }→ ifinter(mem(x, l1), x, l2, l1) :|: z = l1, x >= 0, z' = 1 + x + l2, l1 >= 0, l2 >= 0
inter(z, z') -{ 1 }→ ifinter(mem(x, l2), x, l1, l2) :|: x >= 0, z = 1 + x + l1, z' = l2, l1 >= 0, l2 >= 0
inter(z, z') -{ 1 }→ 0 :|: x >= 0, z = x, z' = 0
inter(z, z') -{ 1 }→ 0 :|: z' = x, x >= 0, z = 0
mem(z, z') -{ 1 }→ ifmem(eq(x, y), x, l) :|: x >= 0, y >= 0, z' = 1 + y + l, l >= 0, z = x
mem(z, z') -{ 1 }→ 0 :|: x >= 0, z = x, z' = 0

Only complete derivations are relevant for the runtime complexity.

(11) CompleteCoflocoProof (EQUIVALENT transformation)

Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V1, V12, V15),0,[inter(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V12, V15),0,[mem(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V12, V15),0,[eq(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V12, V15),0,[ifmem(V, V1, V12, Out)],[V >= 0,V1 >= 0,V12 >= 0]). eq(start(V, V1, V12, V15),0,[ifinter(V, V1, V12, V15, Out)],[V >= 0,V1 >= 0,V12 >= 0,V15 >= 0]). eq(start(V, V1, V12, V15),0,[app(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V12, V15),0,[if(V, V1, V12, Out)],[V >= 0,V1 >= 0,V12 >= 0]). eq(inter(V, V1, Out),1,[mem(V2, V3, Ret0),ifinter(Ret0, V2, V4, V3, Ret)],[Out = Ret,V2 >= 0,V = 1 + V2 + V4,V1 = V3,V4 >= 0,V3 >= 0]). eq(mem(V, V1, Out),1,[eq(V5, V6, Ret01),ifmem(Ret01, V5, V7, Ret1)],[Out = Ret1,V5 >= 0,V6 >= 0,V1 = 1 + V6 + V7,V7 >= 0,V = V5]). eq(eq(V, V1, Out),1,[],[Out = 0,V1 = 1 + V8,V8 >= 0,V = 0]). eq(eq(V, V1, Out),1,[],[Out = 0,V9 >= 0,V = 1 + V9,V1 = 0]). eq(eq(V, V1, Out),1,[eq(V10, V11, Ret2)],[Out = Ret2,V1 = 1 + V11,V10 >= 0,V11 >= 0,V = 1 + V10]). eq(ifmem(V, V1, V12, Out),1,[mem(V13, V14, Ret3)],[Out = Ret3,V1 = V13,V13 >= 0,V14 >= 0,V = 0,V12 = V14]). eq(ifinter(V, V1, V12, V15, Out),1,[inter(V17, V18, Ret11)],[Out = 1 + Ret11 + V16,V1 = V16,V = 1,V16 >= 0,V15 = V18,V12 = V17,V17 >= 0,V18 >= 0]). eq(mem(V, V1, Out),1,[],[Out = 0,V19 >= 0,V = V19,V1 = 0]). eq(app(V, V1, Out),1,[app(V21, V22, Ret12)],[Out = 1 + Ret12 + V20,V20 >= 0,V = 1 + V20 + V21,V1 = V22,V21 >= 0,V22 >= 0]). eq(ifinter(V, V1, V12, V15, Out),1,[inter(V23, V24, Ret4)],[Out = Ret4,V1 = V25,V25 >= 0,V15 = V24,V12 = V23,V23 >= 0,V = 0,V24 >= 0]). eq(ifmem(V, V1, V12, Out),1,[],[Out = 1,V1 = V26,V = 1,V26 >= 0,V27 >= 0,V12 = V27]). eq(eq(V, V1, Out),1,[],[Out = 1,V = 0,V1 = 0]). eq(inter(V, V1, Out),1,[mem(V28, V29, Ret02),ifinter(Ret02, V28, V30, V29, Ret5)],[Out = Ret5,V = V29,V28 >= 0,V1 = 1 + V28 + V30,V29 >= 0,V30 >= 0]). eq(app(V, V1, Out),1,[],[Out = V31,V1 = V31,V31 >= 0,V = 0]). eq(inter(V, V1, Out),1,[],[Out = 0,V32 >= 0,V = V32,V1 = 0]). eq(inter(V, V1, Out),1,[],[Out = 0,V1 = V33,V33 >= 0,V = 0]). eq(if(V, V1, V12, Out),1,[],[Out = V34,V1 = V34,V12 = V35,V = 1,V34 >= 0,V35 >= 0]). eq(if(V, V1, V12, Out),1,[],[Out = V36,V1 = V37,V12 = V36,V37 >= 0,V36 >= 0,V = 0]). input_output_vars(inter(V,V1,Out),[V,V1],[Out]). input_output_vars(mem(V,V1,Out),[V,V1],[Out]). input_output_vars(eq(V,V1,Out),[V,V1],[Out]). input_output_vars(ifmem(V,V1,V12,Out),[V,V1,V12],[Out]). input_output_vars(ifinter(V,V1,V12,V15,Out),[V,V1,V12,V15],[Out]). input_output_vars(app(V,V1,Out),[V,V1],[Out]). input_output_vars(if(V,V1,V12,Out),[V,V1,V12],[Out]).

CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components
0. recursive : [app/3]
1. recursive : [eq/3]
2. non_recursive : [if/4]
3. recursive : [ifmem/4,mem/3]
4. recursive : [ifinter/5,inter/3]
5. non_recursive : [start/4]

#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into app/3
1. SCC is partially evaluated into eq/3
2. SCC is partially evaluated into if/4
3. SCC is partially evaluated into mem/3
4. SCC is partially evaluated into inter/3
5. SCC is partially evaluated into start/4

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations app/3
* CE 25 is refined into CE [28]
* CE 24 is refined into CE [29]


### Cost equations --> "Loop" of app/3
* CEs [29] --> Loop 20
* CEs [28] --> Loop 21

### Ranking functions of CR app(V,V1,Out)
* RF of phase [20]: [V]

#### Partial ranking functions of CR app(V,V1,Out)
* Partial RF of phase [20]:
- RF of loop [20:1]:
V


### Specialization of cost equations eq/3
* CE 21 is refined into CE [30]
* CE 20 is refined into CE [31]
* CE 23 is refined into CE [32]
* CE 22 is refined into CE [33]


### Cost equations --> "Loop" of eq/3
* CEs [33] --> Loop 22
* CEs [30] --> Loop 23
* CEs [31] --> Loop 24
* CEs [32] --> Loop 25

### Ranking functions of CR eq(V,V1,Out)
* RF of phase [22]: [V,V1]

#### Partial ranking functions of CR eq(V,V1,Out)
* Partial RF of phase [22]:
- RF of loop [22:1]:
V
V1


### Specialization of cost equations if/4
* CE 26 is refined into CE [34]
* CE 27 is refined into CE [35]


### Cost equations --> "Loop" of if/4
* CEs [34] --> Loop 26
* CEs [35] --> Loop 27

### Ranking functions of CR if(V,V1,V12,Out)

#### Partial ranking functions of CR if(V,V1,V12,Out)


### Specialization of cost equations mem/3
* CE 17 is refined into CE [36,37]
* CE 19 is refined into CE [38]
* CE 18 is refined into CE [39,40,41,42]


### Cost equations --> "Loop" of mem/3
* CEs [42] --> Loop 28
* CEs [41] --> Loop 29
* CEs [40] --> Loop 30
* CEs [39] --> Loop 31
* CEs [37] --> Loop 32
* CEs [38] --> Loop 33
* CEs [36] --> Loop 34

### Ranking functions of CR mem(V,V1,Out)
* RF of phase [28,29,30]: [V1]
* RF of phase [31]: [V1-1]

#### Partial ranking functions of CR mem(V,V1,Out)
* Partial RF of phase [28,29,30]:
- RF of loop [28:1]:
V1-1
- RF of loop [29:1]:
-V/3+V1/3-1/3
V1/3-2/3
- RF of loop [30:1]:
V1
* Partial RF of phase [31]:
- RF of loop [31:1]:
V1-1


### Specialization of cost equations inter/3
* CE 15 is refined into CE [43]
* CE 16 is refined into CE [44]
* CE 14 is refined into CE [45,46]
* CE 12 is refined into CE [47,48,49]
* CE 13 is refined into CE [50,51]
* CE 11 is refined into CE [52,53,54]


### Cost equations --> "Loop" of inter/3
* CEs [46] --> Loop 35
* CEs [49] --> Loop 36
* CEs [51] --> Loop 37
* CEs [54] --> Loop 38
* CEs [50] --> Loop 39
* CEs [52] --> Loop 40
* CEs [45] --> Loop 41
* CEs [47] --> Loop 42
* CEs [48] --> Loop 43
* CEs [53] --> Loop 44
* CEs [43] --> Loop 45
* CEs [44] --> Loop 46

### Ranking functions of CR inter(V,V1,Out)
* RF of phase [35,36,37,38,39,40,41,42]: [V+V1-1]
* RF of phase [43]: [V]

#### Partial ranking functions of CR inter(V,V1,Out)
* Partial RF of phase [35,36,37,38,39,40,41,42]:
- RF of loop [35:1]:
V-1 depends on loops [37:1,38:1,39:1,40:1]
- RF of loop [36:1]:
V/2-1/2 depends on loops [37:1,38:1,39:1,40:1]
- RF of loop [37:1]:
V+V1-3
- RF of loop [38:1]:
V/2+V1/2-1
- RF of loop [39:1]:
V+V1-1
- RF of loop [40:1]:
V+V1-2
- RF of loop [41:1,42:1]:
V depends on loops [37:1,38:1,39:1,40:1]
* Partial RF of phase [43]:
- RF of loop [43:1]:
V


### Specialization of cost equations start/4
* CE 3 is refined into CE [55,56,57]
* CE 4 is refined into CE [58]
* CE 2 is refined into CE [59,60,61]
* CE 5 is refined into CE [62,63,64,65,66]
* CE 6 is refined into CE [67,68,69]
* CE 7 is refined into CE [70,71,72,73,74]
* CE 8 is refined into CE [75,76,77,78,79,80]
* CE 9 is refined into CE [81,82]
* CE 10 is refined into CE [83,84]


### Cost equations --> "Loop" of start/4
* CEs [80] --> Loop 47
* CEs [68,72,77] --> Loop 48
* CEs [56] --> Loop 49
* CEs [55,57,58,69,73,74,78,79,82,84] --> Loop 50
* CEs [60] --> Loop 51
* CEs [59,64] --> Loop 52
* CEs [61,62,63,65,66,67,70,71,75,76,81,83] --> Loop 53

### Ranking functions of CR start(V,V1,V12,V15)

#### Partial ranking functions of CR start(V,V1,V12,V15)


Computing Bounds
=====================================

#### Cost of chains of app(V,V1,Out):
* Chain [[20],21]: 1*it(20)+1
Such that:it(20) =< -V1+Out

with precondition: [V+V1=Out,V>=1,V1>=0]

* Chain [21]: 1
with precondition: [V=0,V1=Out,V1>=0]


#### Cost of chains of eq(V,V1,Out):
* Chain [[22],25]: 1*it(22)+1
Such that:it(22) =< V

with precondition: [Out=1,V=V1,V>=1]

* Chain [[22],24]: 1*it(22)+1
Such that:it(22) =< V

with precondition: [Out=0,V>=1,V1>=V+1]

* Chain [[22],23]: 1*it(22)+1
Such that:it(22) =< V1

with precondition: [Out=0,V1>=1,V>=V1+1]

* Chain [25]: 1
with precondition: [V=0,V1=0,Out=1]

* Chain [24]: 1
with precondition: [V=0,Out=0,V1>=1]

* Chain [23]: 1
with precondition: [V1=0,Out=0,V>=1]


#### Cost of chains of if(V,V1,V12,Out):
* Chain [27]: 1
with precondition: [V=0,V12=Out,V1>=0,V12>=0]

* Chain [26]: 1
with precondition: [V=1,V1=Out,V1>=0,V12>=0]


#### Cost of chains of mem(V,V1,Out):
* Chain [[31],34]: 3*it(31)+3
Such that:it(31) =< V1

with precondition: [V=0,Out=1,V1>=3]

* Chain [[31],33]: 3*it(31)+1
Such that:it(31) =< V1

with precondition: [V=0,Out=0,V1>=2]

* Chain [[28,29,30],33]: 8*it(28)+3*it(29)+1
Such that:it(29) =< -V/3+V1/3
it(29) =< V1/3
aux(3) =< V1
it(28) =< aux(3)
it(29) =< aux(3)

with precondition: [Out=0,V>=1,V1>=1]

* Chain [[28,29,30],32]: 8*it(28)+3*it(29)+1*s(7)+3
Such that:aux(2) =< -V+V1
s(7) =< V
it(29) =< -V/3+V1/3
aux(1) =< V1
it(28) =< aux(1)
it(29) =< aux(1)
it(28) =< aux(2)
it(29) =< aux(2)

with precondition: [Out=1,V>=1,V1>=V+2]

* Chain [34]: 3
with precondition: [V=0,Out=1,V1>=1]

* Chain [33]: 1
with precondition: [V1=0,Out=0,V>=0]

* Chain [32]: 1*s(7)+3
Such that:s(7) =< V

with precondition: [Out=1,V>=1,V1>=V+1]


#### Cost of chains of inter(V,V1,Out):
* Chain [[43],46]: 3*it(43)+1
Such that:it(43) =< V

with precondition: [V1=0,Out=0,V>=1]

* Chain [[43],45]: 3*it(43)+1
Such that:it(43) =< V

with precondition: [V1=0,Out=0,V>=1]

* Chain [[35,36,37,38,39,40,41,42],46]: 13*it(35)+3*it(36)+17*it(37)+3*it(38)+3*s(59)+8*s(61)+3*s(65)+8*s(66)+3*s(68)+8*s(70)+3*s(74)+8*s(75)+6*s(77)+6*s(79)+1
Such that:it(38) =< V/2+V1/2
aux(81) =< V
aux(82) =< V+V1
aux(83) =< V/2
it(35) =< aux(82)
it(36) =< aux(82)
it(37) =< aux(82)
it(38) =< aux(82)
aux(17) =< aux(82)+1
aux(41) =< aux(82)
aux(28) =< aux(82)* (1/3)
aux(5) =< it(37)*aux(82)
aux(7) =< it(37)*aux(17)
aux(6) =< it(38)*aux(41)
s(77) =< it(37)*aux(17)
aux(40) =< it(38)*aux(17)
s(74) =< it(38)*aux(28)
aux(18) =< aux(5)* (1/2)
s(68) =< aux(5)* (1/3)
aux(20) =< aux(7)* (1/2)
aux(19) =< aux(6)* (1/2)
s(74) =< aux(40)* (1/3)
it(35) =< aux(7)+aux(7)+aux(6)+aux(5)+aux(81)
it(36) =< aux(7)+aux(7)+aux(6)+aux(5)+aux(81)
it(36) =< aux(20)+aux(20)+aux(19)+aux(18)+aux(83)
s(79) =< it(35)*aux(17)
aux(30) =< it(36)*aux(17)
s(65) =< it(36)*aux(28)
s(63) =< it(35)*aux(17)
aux(16) =< it(35)*aux(82)
s(65) =< aux(30)* (1/3)
s(59) =< aux(16)* (1/3)
s(75) =< aux(40)
s(74) =< aux(40)
s(70) =< aux(7)
s(68) =< aux(7)
s(70) =< aux(5)
s(68) =< aux(5)
s(66) =< aux(30)
s(65) =< aux(30)
s(61) =< s(63)
s(59) =< s(63)
s(61) =< aux(16)
s(59) =< aux(16)

with precondition: [V>=1,V1>=1,Out>=0,V+V1>=Out+1,Out+V+V1>=3]

* Chain [[35,36,37,38,39,40,41,42],44,[43],46]: 13*it(35)+3*it(36)+23*it(37)+3*s(59)+8*s(61)+3*s(65)+8*s(66)+3*s(68)+8*s(70)+3*s(74)+8*s(75)+6*s(77)+6*s(79)+4
Such that:aux(84) =< V
aux(85) =< V+V1
aux(86) =< V/2
it(37) =< aux(85)
it(35) =< aux(85)
it(36) =< aux(85)
aux(17) =< aux(85)+1
aux(41) =< aux(85)
aux(28) =< aux(85)* (1/3)
aux(5) =< it(37)*aux(85)
aux(7) =< it(37)*aux(17)
aux(6) =< it(37)*aux(41)
s(77) =< it(37)*aux(17)
aux(40) =< it(37)*aux(17)
s(74) =< it(37)*aux(28)
aux(18) =< aux(5)* (1/2)
s(68) =< aux(5)* (1/3)
aux(20) =< aux(7)* (1/2)
aux(19) =< aux(6)* (1/2)
s(74) =< aux(40)* (1/3)
it(35) =< aux(7)+aux(7)+aux(6)+aux(5)+aux(84)
it(36) =< aux(7)+aux(7)+aux(6)+aux(5)+aux(84)
it(36) =< aux(20)+aux(20)+aux(19)+aux(18)+aux(86)
s(79) =< it(35)*aux(17)
aux(30) =< it(36)*aux(17)
s(65) =< it(36)*aux(28)
s(63) =< it(35)*aux(17)
aux(16) =< it(35)*aux(85)
s(65) =< aux(30)* (1/3)
s(59) =< aux(16)* (1/3)
s(75) =< aux(40)
s(74) =< aux(40)
s(70) =< aux(7)
s(68) =< aux(7)
s(70) =< aux(5)
s(68) =< aux(5)
s(66) =< aux(30)
s(65) =< aux(30)
s(61) =< s(63)
s(59) =< s(63)
s(61) =< aux(16)
s(59) =< aux(16)

with precondition: [V>=1,V1>=1,Out>=0,V+V1>=3,V+V1>=Out+2]

* Chain [[35,36,37,38,39,40,41,42],44,[43],45]: 13*it(35)+3*it(36)+23*it(37)+3*s(59)+8*s(61)+3*s(65)+8*s(66)+3*s(68)+8*s(70)+3*s(74)+8*s(75)+6*s(77)+6*s(79)+4
Such that:aux(87) =< V
aux(88) =< V+V1
aux(89) =< V/2
it(37) =< aux(88)
it(35) =< aux(88)
it(36) =< aux(88)
aux(17) =< aux(88)+1
aux(41) =< aux(88)
aux(28) =< aux(88)* (1/3)
aux(5) =< it(37)*aux(88)
aux(7) =< it(37)*aux(17)
aux(6) =< it(37)*aux(41)
s(77) =< it(37)*aux(17)
aux(40) =< it(37)*aux(17)
s(74) =< it(37)*aux(28)
aux(18) =< aux(5)* (1/2)
s(68) =< aux(5)* (1/3)
aux(20) =< aux(7)* (1/2)
aux(19) =< aux(6)* (1/2)
s(74) =< aux(40)* (1/3)
it(35) =< aux(7)+aux(7)+aux(6)+aux(5)+aux(87)
it(36) =< aux(7)+aux(7)+aux(6)+aux(5)+aux(87)
it(36) =< aux(20)+aux(20)+aux(19)+aux(18)+aux(89)
s(79) =< it(35)*aux(17)
aux(30) =< it(36)*aux(17)
s(65) =< it(36)*aux(28)
s(63) =< it(35)*aux(17)
aux(16) =< it(35)*aux(88)
s(65) =< aux(30)* (1/3)
s(59) =< aux(16)* (1/3)
s(75) =< aux(40)
s(74) =< aux(40)
s(70) =< aux(7)
s(68) =< aux(7)
s(70) =< aux(5)
s(68) =< aux(5)
s(66) =< aux(30)
s(65) =< aux(30)
s(61) =< s(63)
s(59) =< s(63)
s(61) =< aux(16)
s(59) =< aux(16)

with precondition: [V>=1,V1>=1,Out>=0,V+V1>=3,V+V1>=Out+2]

* Chain [[35,36,37,38,39,40,41,42],44,46]: 13*it(35)+3*it(36)+17*it(37)+3*it(38)+3*s(59)+8*s(61)+3*s(65)+8*s(66)+3*s(68)+8*s(70)+3*s(74)+8*s(75)+6*s(77)+6*s(79)+4
Such that:it(38) =< V/2+V1/2
aux(90) =< V
aux(91) =< V+V1
aux(92) =< V/2
it(35) =< aux(91)
it(36) =< aux(91)
it(37) =< aux(91)
it(38) =< aux(91)
aux(17) =< aux(91)+1
aux(41) =< aux(91)
aux(28) =< aux(91)* (1/3)
aux(5) =< it(37)*aux(91)
aux(7) =< it(37)*aux(17)
aux(6) =< it(38)*aux(41)
s(77) =< it(37)*aux(17)
aux(40) =< it(38)*aux(17)
s(74) =< it(38)*aux(28)
aux(18) =< aux(5)* (1/2)
s(68) =< aux(5)* (1/3)
aux(20) =< aux(7)* (1/2)
aux(19) =< aux(6)* (1/2)
s(74) =< aux(40)* (1/3)
it(35) =< aux(7)+aux(7)+aux(6)+aux(5)+aux(90)
it(36) =< aux(7)+aux(7)+aux(6)+aux(5)+aux(90)
it(36) =< aux(20)+aux(20)+aux(19)+aux(18)+aux(92)
s(79) =< it(35)*aux(17)
aux(30) =< it(36)*aux(17)
s(65) =< it(36)*aux(28)
s(63) =< it(35)*aux(17)
aux(16) =< it(35)*aux(91)
s(65) =< aux(30)* (1/3)
s(59) =< aux(16)* (1/3)
s(75) =< aux(40)
s(74) =< aux(40)
s(70) =< aux(7)
s(68) =< aux(7)
s(70) =< aux(5)
s(68) =< aux(5)
s(66) =< aux(30)
s(65) =< aux(30)
s(61) =< s(63)
s(59) =< s(63)
s(61) =< aux(16)
s(59) =< aux(16)

with precondition: [V>=1,V1>=1,Out>=0,V+V1>=Out+1,Out+V+V1>=3]

* Chain [[35,36,37,38,39,40,41,42],44,45]: 13*it(35)+3*it(36)+17*it(37)+3*it(38)+3*s(59)+8*s(61)+3*s(65)+8*s(66)+3*s(68)+8*s(70)+3*s(74)+8*s(75)+6*s(77)+6*s(79)+4
Such that:it(38) =< V/2+V1/2
aux(93) =< V
aux(94) =< V+V1
aux(95) =< V/2
it(35) =< aux(94)
it(36) =< aux(94)
it(37) =< aux(94)
it(38) =< aux(94)
aux(17) =< aux(94)+1
aux(41) =< aux(94)
aux(28) =< aux(94)* (1/3)
aux(5) =< it(37)*aux(94)
aux(7) =< it(37)*aux(17)
aux(6) =< it(38)*aux(41)
s(77) =< it(37)*aux(17)
aux(40) =< it(38)*aux(17)
s(74) =< it(38)*aux(28)
aux(18) =< aux(5)* (1/2)
s(68) =< aux(5)* (1/3)
aux(20) =< aux(7)* (1/2)
aux(19) =< aux(6)* (1/2)
s(74) =< aux(40)* (1/3)
it(35) =< aux(7)+aux(7)+aux(6)+aux(5)+aux(93)
it(36) =< aux(7)+aux(7)+aux(6)+aux(5)+aux(93)
it(36) =< aux(20)+aux(20)+aux(19)+aux(18)+aux(95)
s(79) =< it(35)*aux(17)
aux(30) =< it(36)*aux(17)
s(65) =< it(36)*aux(28)
s(63) =< it(35)*aux(17)
aux(16) =< it(35)*aux(94)
s(65) =< aux(30)* (1/3)
s(59) =< aux(16)* (1/3)
s(75) =< aux(40)
s(74) =< aux(40)
s(70) =< aux(7)
s(68) =< aux(7)
s(70) =< aux(5)
s(68) =< aux(5)
s(66) =< aux(30)
s(65) =< aux(30)
s(61) =< s(63)
s(59) =< s(63)
s(61) =< aux(16)
s(59) =< aux(16)

with precondition: [V>=1,V1>=1,Out>=0,V+V1>=Out+1,Out+V+V1>=3]

* Chain [46]: 1
with precondition: [V=0,Out=0,V1>=0]

* Chain [45]: 1
with precondition: [V1=0,Out=0,V>=0]

* Chain [44,[43],46]: 3*it(43)+4
Such that:it(43) =< V1

with precondition: [V=0,Out=0,V1>=2]

* Chain [44,[43],45]: 3*it(43)+4
Such that:it(43) =< V1

with precondition: [V=0,Out=0,V1>=2]

* Chain [44,46]: 4
with precondition: [V=0,Out=0,V1>=1]

* Chain [44,45]: 4
with precondition: [V=0,Out=0,V1>=1]


#### Cost of chains of start(V,V1,V12,V15):
* Chain [53]: 9*s(237)+97*s(238)+26*s(239)+6*s(240)+30*s(247)+6*s(248)+15*s(250)+12*s(253)+6*s(255)+6*s(258)+16*s(259)+40*s(260)+16*s(261)+16*s(262)+39*s(263)+9*s(264)+9*s(267)+18*s(269)+9*s(271)+9*s(274)+24*s(275)+24*s(276)+24*s(277)+14*s(278)+3*s(280)+3*s(284)+14*s(287)+8*s(288)+5
Such that:s(283) =< -V1+V12
s(234) =< V12+V15
s(235) =< V12/2
s(236) =< V12/2+V15/2
s(280) =< V12/3
aux(102) =< V1
aux(103) =< -V1/3+V12/3
aux(104) =< V12
s(287) =< aux(102)
s(280) =< aux(103)
s(284) =< aux(103)
s(278) =< aux(104)
s(288) =< aux(104)
s(284) =< aux(104)
s(288) =< s(283)
s(284) =< s(283)
s(280) =< aux(104)
s(237) =< s(236)
s(238) =< s(234)
s(239) =< s(234)
s(240) =< s(234)
s(241) =< s(234)+1
s(242) =< s(234)
s(243) =< s(234)* (1/3)
s(244) =< s(238)*s(234)
s(245) =< s(238)*s(241)
s(246) =< s(238)*s(242)
s(247) =< s(238)*s(241)
s(248) =< s(238)*s(243)
s(249) =< s(244)* (1/2)
s(250) =< s(244)* (1/3)
s(251) =< s(245)* (1/2)
s(252) =< s(246)* (1/2)
s(248) =< s(245)* (1/3)
s(239) =< s(245)+s(245)+s(246)+s(244)+aux(104)
s(240) =< s(245)+s(245)+s(246)+s(244)+aux(104)
s(240) =< s(251)+s(251)+s(252)+s(249)+s(235)
s(253) =< s(239)*s(241)
s(254) =< s(240)*s(241)
s(255) =< s(240)*s(243)
s(256) =< s(239)*s(241)
s(257) =< s(239)*s(234)
s(255) =< s(254)* (1/3)
s(258) =< s(257)* (1/3)
s(259) =< s(245)
s(248) =< s(245)
s(260) =< s(245)
s(250) =< s(245)
s(260) =< s(244)
s(250) =< s(244)
s(261) =< s(254)
s(255) =< s(254)
s(262) =< s(256)
s(258) =< s(256)
s(262) =< s(257)
s(258) =< s(257)
s(263) =< s(234)
s(264) =< s(234)
s(237) =< s(234)
s(265) =< s(237)*s(242)
s(266) =< s(237)*s(241)
s(267) =< s(237)*s(243)
s(268) =< s(265)* (1/2)
s(267) =< s(266)* (1/3)
s(263) =< s(245)+s(245)+s(265)+s(244)+aux(104)
s(264) =< s(245)+s(245)+s(265)+s(244)+aux(104)
s(264) =< s(251)+s(251)+s(268)+s(249)+s(235)
s(269) =< s(263)*s(241)
s(270) =< s(264)*s(241)
s(271) =< s(264)*s(243)
s(272) =< s(263)*s(241)
s(273) =< s(263)*s(234)
s(271) =< s(270)* (1/3)
s(274) =< s(273)* (1/3)
s(275) =< s(266)
s(267) =< s(266)
s(276) =< s(270)
s(271) =< s(270)
s(277) =< s(272)
s(274) =< s(272)
s(277) =< s(273)
s(274) =< s(273)

with precondition: [V=0,V1>=0]

* Chain [52]: 6*s(294)+5
Such that:s(293) =< V15
s(294) =< s(293)

with precondition: [V=0,V12=0,V1>=0]

* Chain [51]: 6*s(296)+2
Such that:s(295) =< V12
s(296) =< s(295)

with precondition: [V=0,V15=0,V1>=0,V12>=0]

* Chain [50]: 6*s(298)+9*s(303)+97*s(304)+26*s(305)+6*s(306)+30*s(313)+6*s(314)+15*s(316)+12*s(319)+6*s(321)+6*s(324)+16*s(325)+40*s(326)+16*s(327)+16*s(328)+39*s(329)+9*s(330)+9*s(333)+18*s(335)+9*s(337)+9*s(340)+24*s(341)+24*s(342)+24*s(343)+9*s(348)+97*s(349)+26*s(350)+6*s(351)+30*s(358)+6*s(359)+15*s(361)+12*s(364)+6*s(366)+6*s(369)+16*s(370)+40*s(371)+16*s(372)+16*s(373)+39*s(374)+9*s(375)+9*s(378)+18*s(380)+9*s(382)+9*s(385)+24*s(386)+24*s(387)+24*s(388)+3*s(389)+9*s(391)+3*s(393)+4*s(396)+8*s(397)+5
Such that:s(392) =< -V+V1
s(345) =< V+V1
s(346) =< V/2
s(347) =< V/2+V1/2
s(389) =< V1/3
s(299) =< V12
s(300) =< V12+V15
s(301) =< V12/2
s(302) =< V12/2+V15/2
s(297) =< V15
aux(105) =< V
aux(106) =< -V/3+V1/3
aux(107) =< V1
s(396) =< aux(105)
s(389) =< aux(106)
s(393) =< aux(106)
s(391) =< aux(107)
s(397) =< aux(107)
s(393) =< aux(107)
s(397) =< s(392)
s(393) =< s(392)
s(348) =< s(347)
s(349) =< s(345)
s(350) =< s(345)
s(351) =< s(345)
s(352) =< s(345)+1
s(353) =< s(345)
s(354) =< s(345)* (1/3)
s(355) =< s(349)*s(345)
s(356) =< s(349)*s(352)
s(357) =< s(349)*s(353)
s(358) =< s(349)*s(352)
s(359) =< s(349)*s(354)
s(360) =< s(355)* (1/2)
s(361) =< s(355)* (1/3)
s(362) =< s(356)* (1/2)
s(363) =< s(357)* (1/2)
s(359) =< s(356)* (1/3)
s(350) =< s(356)+s(356)+s(357)+s(355)+aux(105)
s(351) =< s(356)+s(356)+s(357)+s(355)+aux(105)
s(351) =< s(362)+s(362)+s(363)+s(360)+s(346)
s(364) =< s(350)*s(352)
s(365) =< s(351)*s(352)
s(366) =< s(351)*s(354)
s(367) =< s(350)*s(352)
s(368) =< s(350)*s(345)
s(366) =< s(365)* (1/3)
s(369) =< s(368)* (1/3)
s(370) =< s(356)
s(359) =< s(356)
s(371) =< s(356)
s(361) =< s(356)
s(371) =< s(355)
s(361) =< s(355)
s(372) =< s(365)
s(366) =< s(365)
s(373) =< s(367)
s(369) =< s(367)
s(373) =< s(368)
s(369) =< s(368)
s(374) =< s(345)
s(375) =< s(345)
s(348) =< s(345)
s(376) =< s(348)*s(353)
s(377) =< s(348)*s(352)
s(378) =< s(348)*s(354)
s(379) =< s(376)* (1/2)
s(378) =< s(377)* (1/3)
s(374) =< s(356)+s(356)+s(376)+s(355)+aux(105)
s(375) =< s(356)+s(356)+s(376)+s(355)+aux(105)
s(375) =< s(362)+s(362)+s(379)+s(360)+s(346)
s(380) =< s(374)*s(352)
s(381) =< s(375)*s(352)
s(382) =< s(375)*s(354)
s(383) =< s(374)*s(352)
s(384) =< s(374)*s(345)
s(382) =< s(381)* (1/3)
s(385) =< s(384)* (1/3)
s(386) =< s(377)
s(378) =< s(377)
s(387) =< s(381)
s(382) =< s(381)
s(388) =< s(383)
s(385) =< s(383)
s(388) =< s(384)
s(385) =< s(384)
s(389) =< aux(107)
s(303) =< s(302)
s(304) =< s(300)
s(305) =< s(300)
s(306) =< s(300)
s(307) =< s(300)+1
s(308) =< s(300)
s(309) =< s(300)* (1/3)
s(310) =< s(304)*s(300)
s(311) =< s(304)*s(307)
s(312) =< s(304)*s(308)
s(313) =< s(304)*s(307)
s(314) =< s(304)*s(309)
s(315) =< s(310)* (1/2)
s(316) =< s(310)* (1/3)
s(317) =< s(311)* (1/2)
s(318) =< s(312)* (1/2)
s(314) =< s(311)* (1/3)
s(305) =< s(311)+s(311)+s(312)+s(310)+s(299)
s(306) =< s(311)+s(311)+s(312)+s(310)+s(299)
s(306) =< s(317)+s(317)+s(318)+s(315)+s(301)
s(319) =< s(305)*s(307)
s(320) =< s(306)*s(307)
s(321) =< s(306)*s(309)
s(322) =< s(305)*s(307)
s(323) =< s(305)*s(300)
s(321) =< s(320)* (1/3)
s(324) =< s(323)* (1/3)
s(325) =< s(311)
s(314) =< s(311)
s(326) =< s(311)
s(316) =< s(311)
s(326) =< s(310)
s(316) =< s(310)
s(327) =< s(320)
s(321) =< s(320)
s(328) =< s(322)
s(324) =< s(322)
s(328) =< s(323)
s(324) =< s(323)
s(329) =< s(300)
s(330) =< s(300)
s(303) =< s(300)
s(331) =< s(303)*s(308)
s(332) =< s(303)*s(307)
s(333) =< s(303)*s(309)
s(334) =< s(331)* (1/2)
s(333) =< s(332)* (1/3)
s(329) =< s(311)+s(311)+s(331)+s(310)+s(299)
s(330) =< s(311)+s(311)+s(331)+s(310)+s(299)
s(330) =< s(317)+s(317)+s(334)+s(315)+s(301)
s(335) =< s(329)*s(307)
s(336) =< s(330)*s(307)
s(337) =< s(330)*s(309)
s(338) =< s(329)*s(307)
s(339) =< s(329)*s(300)
s(337) =< s(336)* (1/3)
s(340) =< s(339)* (1/3)
s(341) =< s(332)
s(333) =< s(332)
s(342) =< s(336)
s(337) =< s(336)
s(343) =< s(338)
s(340) =< s(338)
s(343) =< s(339)
s(340) =< s(339)
s(298) =< s(297)

with precondition: [V>=1,V1>=0]

* Chain [49]: 6*s(402)+2
Such that:s(401) =< V12
s(402) =< s(401)

with precondition: [V=1,V15=0,V1>=0,V12>=0]

* Chain [48]: 6*s(404)+1
Such that:s(403) =< V
s(404) =< s(403)

with precondition: [V1=0,V>=0]

* Chain [47]: 1*s(405)+1
Such that:s(405) =< V1

with precondition: [V=V1,V>=1]


Closed-form bounds of start(V,V1,V12,V15):
-------------------------------------
* Chain [53] with precondition: [V=0,V1>=0]
- Upper bound: 14*V1+5+nat(V12)*22+nat(V12+V15)*373+nat(V12+V15)*213*nat(V12+V15)+nat(V12+V15)*27*nat(V12/2+V15/2)+nat(V12/2+V15/2)*33+nat(-V1/3+V12/3)*3+nat(V12/3)*3
- Complexity: n^2
* Chain [52] with precondition: [V=0,V12=0,V1>=0]
- Upper bound: nat(V15)*6+5
- Complexity: n
* Chain [51] with precondition: [V=0,V15=0,V1>=0,V12>=0]
- Upper bound: 6*V12+2
- Complexity: n
* Chain [50] with precondition: [V>=1,V1>=0]
- Upper bound: 4*V+17*V1+5+nat(V15)*6+ (373*V+373*V1)+ (213*V+213*V1)* (V+V1)+ (V/2+V1/2)* (27*V+27*V1)+nat(V12+V15)*373+nat(V12+V15)*213*nat(V12+V15)+nat(V12+V15)*27*nat(V12/2+V15/2)+ (33/2*V+33/2*V1)+nat(V12/2+V15/2)*33+nat(-V/3+V1/3)*3+V1
- Complexity: n^2
* Chain [49] with precondition: [V=1,V15=0,V1>=0,V12>=0]
- Upper bound: 6*V12+2
- Complexity: n
* Chain [48] with precondition: [V1=0,V>=0]
- Upper bound: 6*V+1
- Complexity: n
* Chain [47] with precondition: [V=V1,V>=1]
- Upper bound: V1+1
- Complexity: n

### Maximum cost of start(V,V1,V12,V15): max([max([6*V,nat(V12)*6+1,nat(V15)*6+4]),13*V1+4+nat(V12+V15)*373+nat(V12+V15)*213*nat(V12+V15)+nat(V12+V15)*27*nat(V12/2+V15/2)+nat(V12/2+V15/2)*33+max([nat(-V1/3+V12/3)*3+nat(V12)*22+nat(V12/3)*3,4*V+3*V1+nat(V15)*6+ (373*V+373*V1)+ (213*V+213*V1)* (V+V1)+ (V/2+V1/2)* (27*V+27*V1)+ (33/2*V+33/2*V1)+nat(-V/3+V1/3)*3+V1])+V1])+1
Asymptotic class: n^2
* Total analysis performed in 1692 ms.

(12) BOUNDS(1, n^2)